Nuprl Lemma : d-single-rframe_wf 0,22

i:Id, L:Knd List, x:Id. @i: only members of L read x  Dsys 
latex


DefinitionsId, t  T, Knd, type List, , x:AB(x), only members of L read x, MsgA, IdDeq, eqof(d), f(a), if b t else f fi, x.A(x), @i: only members of L read x, Dsys
Lemmasifthenelse wf, eqof wf, id-deq wf, msga wf, ma-single-rframe wf, ma-empty wf, Knd wf, Id wf

origin